Inference at * 1 
Iof proof for Lemma branch-ifthenelse:



1. b : 
2. P : Top
3. Q : Top
  if x:b then P else Q fi  ~ if b then P else Q fi  

latex

 by ((Branch 0) 
CollapseTHENA (Auto)) 

latex

Co1: 

Co1: 4. x : b
Co1: 5. bool-decider(b) = (inl x )
Co1:   P ~ if b then P else Q fi 
Co2: 

Co2: 4. y : (b)
Co2: 5. bool-decider(b) = (inr y )
Co2:   Q ~ if b then P else Q fi 
Co.

Definitions	if p:P then A(p) else B fi , , s = t, P  Q, x:AB(x), bool-decider(b), t  T, b, x:A. B(x), Dec(P), P  Q, left + right
Lemmas	bool-decider wf, decidable wf, assert wf